| Definitions | t  T, World, FairFifo, E, IdLnk, m(i;t), onlnk(l;mss), w_sends(e;l), <a,b>, Msg, type List, s = t, f(a), 1of(t), e <c e', a<b, P   Q, sends(l;e), ||as||, #$n, {i..j },  x:A. B(x), {x:A| B(x) }, x:A  B(x), Prop, False,  A, P & Q, A B, i j < k,  , index(e), {T}, P  Q, x:A B(x), left+right, P  Q, P Q, A & B,  x:A. B(x), sender(e), kind(e), lnk(k), Type, isrcv(k),  b, val(e), tag(k), msg(l;t;v), l[i], w.M, Msg(M), Void, True,  T, SQType(T), s ~ t, S  T, upto(n),  x.A(x), map(f;as), w-info(w;e), rmsg(info;val;e), f o g,  x:A. B(x), Top, i j,  , V(i;k), Id, rtag(info;e), link(e), time(e), loc(e), rcv?(e), 2of(t), act(k), islocal(k), kindcase(k; a.f(a); l,t.g(l;t) ), Knd, ecase1(e;info;i.f(i);l,e'.g(l;e')),  x. t(x), rcv(l,tg), strong-subtype(A;B), a(i;t), isnull(a), EqDecider(T), NatDeq, IdDeq, product-deq(A;B;a;b), receives(dE;dL;pred?;info;p;e;l), IdLnkDeq, rcv-from-on(dE;dL;info;e;l;r), sends(dE;dL;pred?;info;val;p;e;l), EOrderAxioms(E; pred?; info), w-pred(w;e), w-order-axioms, pred(e), first(e), SWellFounded(R(x;y)), sender(e), pred!(e;e'), xL. P(x), sends-bound(p;e;l), eventlist(pred?;e), (x l), x before y l, no_repeats(T;l), R^*, x f y, destination(l), loc(e), e < e', Atom$n, Dec(P), e <loc e', R^+, locl(a), isl(x),  , if b t else f fi, Case b of inl(x) s(x) ; inr(y) t(y) |
| Lemmas | before-upto, w-cless-loc, w-loc wf, before-map, w locl-lemma, l before member, l before member2, l before eventlist iff, w-locl wf, w-sends-fifo1, decidable lt, w-time wf, member upto, Id sq, rcv?-link, cless wf, loc wf, ldst wf, w locle-lemma, member eventlist, member map, no repeats eventlist, implies-filter-equal, l before wf, l member wf, member filter, eventlist wf, sends-bound wf, list-equal-set, receives wf, first wf, pred wf, rcv? wf, sender wf, w-order-axioms, EOrderAxioms wf, w-pred wf, assert-rcv-from-on, map wf, rcv-from-on wf, idlnk-deq wf, product-deq wf, id-deq wf, nat-deq wf, strong-subtype-deq-subtype, strong-subtype-set3, not wf, w-isnull wf, w-a wf, pi2 wf, strong-subtype-self, nat wf, Knd sq, w-loc-lemma, w-loc-rcv, w-E sq, pi1 wf, Knd wf, false wf, subtype rel self, rcv?-kind, w-kind-lemma, msg wf, link wf, rtag wf, Id wf, w-info wf, w-eval wf, map-map, upto wf, top wf, non neg length, map-upto-length, w sends wf, true wf, IdLnk sq, w-sends-msg, select wf, squash wf, le wf, Msg wf, w-M wf, assert wf, isrcv wf, w-index wf, lnk wf, w-ekind wf, w-sender wf, w-sends-fifo, w-causl wf, int seg wf, length wf1, w-Msg wf, w-sends wf, IdLnk wf, w-E wf, fair-fifo wf, world wf, w-sends-reliable |